[TS Calls] Execute semantic models written in TypeScript - #380

Summary

Execute semantic models written in ordinary TypeScript through the existing EtsIR interpreter. Array.pop uses array indexing and length, preserving numeric, reference, and unresolved elements, mutations, and aliases.

• Load and validate static model entry points with the native JacoDB TypeScript frontend.
• Keep an immutable EtsIR JSON snapshot and materialize a separate object graph for each machine. Models sharing a source file share one materialized file within that machine.
• Bind receiver and arguments through ordinary call frames; preserve returns, exceptions, nested dispatch, and recursion prevention.
• Preserve domain guards, residual fallback, automatic built-in discovery, selected IDs, and signature-collision checks. Model declarations cannot bypass guards through application method lookup.
• Write array length through the normalized storage type. Read numeric fake-value payloads from current memory with their runtime-kind guard, so numeric any values and symbolic any[] pop results can shrink arrays. Negative zero remains accepted.
• Apply length constraints through scope.assert, which updates both path constraints and cached models and stops infeasible paths.

The branch is based on main at a442b2a9, including #377.

Supported domain

The built-in pop model accepts zero-argument calls on proven one-dimensional arrays, including any[], unknown[], and normalized widened/wrapped aliases. Unsupported inputs use the configured fallback.

Length assignments support integral numeric values from zero through the current length, within the configured size limit. Growth and coercion of nonnumeric lengths remain unsupported; growth and sparse slots are tracked in #388.

Validation

For head 8188fecd:

• 54 focused artifact, pop, shift, and EtsIR execution tests passed.
• 13 catalog tests passed in a separate process. Local JDK 23 required MockK self-attach flags.
• The new regression checks cached-model validity after assigning an unconstrained any value to array length, with soft-constraint repair disabled. Temporarily replacing both assertions with direct pathConstraints += made that regression fail; the committed implementation retains scope.assert.
• :usvm-ts:detektMain and :usvm-ts:detektTest passed with 0 smells; git diff --check passed.
• Full CI for this head passed: core, JVM, Python, TypeScript, TS PBT, and lint.

Closes #366

Part of #360